i, j:, F:({i..j}{u}). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k)) 

latex

Up	int 2, int 2
Definitions	t  T, x(s), P  Q, , x:A. B(x), x. t(x), Dec(P), P  Q, A, x:A. B(x), False, P & Q, P  Q
Lemmas	decidable wf, int seg wf, decidable not, not wf, decidable ex int seg, dneg elim a, all functionality wrt iff, not over exists, iff transitivity